Electronic circuits have become ubiquitous in modern society. The electronics industry routinely announces accelerated clocking speeds, higher transmission frequencies, and more complex integrated circuit modules. While the benefits of these devices are myriad, the sheer complexity is becoming overwhelming. Design and verification of such devices requires the development of efficient algorithms for solving formulas describing design properties. An important class of formulas that needs to be solved efficiently is quantified Boolean formulas.
Additional background may be found in the following references, which are hereby incorporate in their entirety: A. Biere, “PicoSAT Essentials”, JSAT, vol. 4, no. 2-4, pp. 75-97, 2008; J. Brauer, A. King, and J. Kriener, “Existential Quantification as Incremental SAT”, Proc. CAV-2011; R. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Trans. on Computers, vol. C-35, no. 8, pp. 677-691, 1986; E. Clarke, O. Grumberg, and D. Peled. Model Checking, MIT Press, 2000; M. Davis, and H. Putnam, “A Computing Procedure for Quantification Theory”, J. ACM, vol. 7, no. 3, pp. 201-215, July, 1960; M. Ganai, “Propelling SAT and SAT-based BMC using Careset”, in Proc. FMCAD-2010, pp. 231-238; M. Ganai, A. Gupta, and P. Ashar, “Efficient SAT-based unbounded symbolic model checking using circuit cofactoring”, in Proc. ICCAD-2004, pp. 510-517; E. Goldberg, and P. Manolios, “SAT-solving Based on Boundary Point Elimination”, in Proc. HVC-2010, LNCS vol. 6504, pp. 93-111; E. Goldberg, M. Prasad, and R. Brayton, “Using Problem Symmetry in Search Based Satisfiability Algorithms”, in DATE-2002, pp. 134-141; E. Goldberg, “Boundary points and resolution”, in Proc. SAT-2009, LNCS, vol. 5584, pp. 147-160; H. Jin, and F. Somenzi, “Prime clauses for fast enumeration of satisfying assignments to Boolean circuits,” in Proc. DAC-2005, pp. 750-753; K. McMillan, “Interpolation and SAT-Based Model Checking,” in Proc. CAV-2003, LNCS, vol. 2725, pp. 1-13; K. McMillan, “Applying SAT Methods in Unbounded Symbolic Model Checking,” in Proc. CAV-2002, pp. 250-264; K. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993; HWMCC-2010 benchmarks, http://fmv.jku.at/hwmcc10/benchmarks.html.